#define USERS	2
/* Bidder1 States */

mtype = {idleB, startB, submittedB};

/* Auctioneer States */

mtype ={waitA, startA, processBidA, endA};

/* Events*/

mtype = {start_auction, auction_started, status, winner, loser, end_auction, dummy, send_bid, danger};

mtype stateA;
bool gUp[USERS];
int amountGivenUp;
bool dang = false;

/* channels for transitions */	

int amountOfClients = USERS;
int startBid=13;
int nrounds = 5;

chan m2A = [0] of {int, mtype};
chan m2B[USERS] = [1] of {int, mtype};

/* Stuff for LTL */
bool someoneWon = false;
int bids[USERS];
int max_id = -1;

init {
    int i = 0;
    do
    :: (i<amountOfClients) -> run client(i); gUp[i] = false;
        i = i+1;
    :: (i==amountOfClients) -> break;
    od;
    run auctioneer();
    m2A!0, start_auction;
    printf("Msg to start the auction\n");
}

/*Client process*/

proctype client(int id) {
    mtype stateB = idleB;
    int bid_limit;
    atomic {
	if
	:: skip -> bid_limit = 25;
	:: skip -> bid_limit = 26;
	:: skip -> bid_limit = 27;
	fi;
    }
    
    int max_bid;
    do
    :: m2B[id]?0, auction_started ->
        printf("The auction is now open, the client %d knows",id);
    :: m2B[id]?0, end_auction -> printf("Auction is terminating \n");
        break;
    :: m2B[id]?max_bid,send_bid -> printf("Ready to submit a bid\n");
        printf("Sending bid \n");
        atomic {
            if
            :: (bid_limit >= (max_bid+1)) -> m2A!(max_bid+1), dummy; bids[id] = max_bid+1;
            :: (bid_limit >= (max_bid+2)) -> m2A!(max_bid+2), dummy; bids[id] = max_bid+2;
            :: (bid_limit >= (max_bid+3)) -> m2A!(max_bid+3), dummy; bids[id] = max_bid+3;
            :: (bid_limit >= (max_bid+4)) -> m2A!(max_bid+4), dummy; bids[id] = max_bid+4;
            :: (bid_limit >= (max_bid+5)) -> m2A!(max_bid+5), dummy; bids[id] = max_bid+5;
	    :: (bid_limit < (max_bid+1) && amountGivenUp<amountOfClients) -> gUp[id] = true; amountGivenUp=amountGivenUp+1;
                printf("Player %d has given Up\n",id); m2A!0,dummy;
            fi;
        }
        stateB = submittedB;
        printf("Bid submitted\n");
        printf("Waiting for the result now\n");
    ::m2B[id]?0, status -> printf("Added Bid\n");
        stateB = idleB;
    ::m2B[id]?0, winner->
        printf("Hurray, I won\n");
        stateB = idleB;
    ::m2B[id]?0, loser ->
        printf("I lost :(\n");
        stateB = idleB;
    ::m2B[id]?0, danger ->
        printf("Auction Shutdown\n");
	break;
    od;
}


/*Auction process*/

proctype auctioneer() {
    int round = 0;
    int max_bid = startBid;
    int i = 0;
    stateA = waitA;
    int bid;
    int id;
    do
    :: (id<amountOfClients && stateA!=endA) ->
        if
        :: (((amountOfClients-1)==amountGivenUp) || (round==nrounds)) -> stateA=endA;
        :: else -> skip;
        fi;
        do 
        :: dang -> /* Gör nåt */
            do
            :: (i<amountOfClients && gUp[i]) -> m2B[i]!0,danger;i = i + 1;
            :: (i==amountOfClients) -> i = 0; break;
            od;
        :: (stateA == waitA && !dang) -> printf("Waiting to start the auction\n");
            m2A?0, start_auction;
            printf("Ready to get the auction started\n");
            do
            :: (i<amountOfClients) -> m2B[i]!0,auction_started;
                i = i+1;
            :: (i==amountOfClients) -> i = 0;
                break;
            od;
            stateA = startA;
            printf("Sending start signal\n");
        :: (stateA == startA && !dang) -> printf("Should Player %d submit a bid\n",id);
            if
            :: gUp[id] || max_id==id -> break;
            :: else -> skip;
            fi;
            m2B[id]!max_bid,send_bid;
            printf("Waiting for a bid to be submitted by %d....\n",id);
            m2A?bid, dummy;
            printf("Client bid received\n");
            stateA=processBidA;
        :: (stateA == processBidA && !dang) -> printf("Computing if it is winning bid\n");
            if
            :: bid>max_bid && bid>=startBid -> m2B[id]!0, status; max_bid = bid; max_id=id;
            :: bid<startBid && bid!=0 -> m2B[id]!0, status;
            :: bid == 0 -> m2B[id]!0,loser;
            fi;
            stateA = startA;
        :: (stateA == endA && !dang) -> printf("Winner elected.Auction will terminate\n");
            do
            :: (i<amountOfClients && i!=max_id && !gUp[i]) -> 
                m2B[i]!0,loser;
                m2B[i]!0,end_auction;
                i = i+1;
            :: (i<amountOfClients && gUp[i]) -> m2B[i]!0,end_auction;i = i + 1;
            :: (i==max_id) -> i = i + 1;
            :: (i==amountOfClients) -> i = 0; break;
            od;
            m2B[max_id]!0,winner;
            someoneWon = true;
            m2B[max_id]!0,end_auction;
            break;
        od;
        id = id + 1;
    :: (id==amountOfClients && stateA!=endA) -> round = round + 1; id = 0; printf("NEW ROUND: %d \n",round);
    :: (stateA==endA) -> break;
    od;
    printf("Shutting down auctioneer\n");
}

//ltl i {[]<> someoneWon}
//ltl ii {[] ((bids[0]>bids[1]) -> (<> (someoneWon && max_id==0)))}
//ltl iii1 {!someoneWon U (amountGivenUp==1)}
//ltl iii2 {!someoneWon U (amountGivenUp==(amountOfClients-1))}
ltl iv {[](!dang -> (<> (someoneWon && (max_id==0 || max_id==1)))}
